\begin{tabbing}
$\forall$$T$,$A$:Type, $f$:($A$$\rightarrow$$T$), $l$:IdLnk.
\\[0ex]normal{-}type\=\{i:l\}\+
\\[0ex]($A$)
\-\\[0ex]$\Rightarrow$ normal{-}type\=\{i:l\}\+
\\[0ex]($T$)
\-\\[0ex]$\Rightarrow$ (send\_onceR\{done:ut2, tg:ut2, b:ut2, done1:ut2\}($T$; $A$; $f$; $l$) $\in$ es\_realizer\{i:l\})
\end{tabbing}